es:ES, e1, e2:E, P:(discrete state@loc(e1)).
e[e1,e2).P((discrete state after e))  e(e1,e2].P((discrete state when e)) 

latex

Definitions

f(a), EState(T), Id, , x:AB(x), t  T, x:A. B(x), pred!(e;e'), SWellFounded(R(x;y)), Unit, Void, x:A.B(x), Top, S  T, left + right, Type, suptype(S; T), first(e), b, A, loc(e), <a, b>, s = t, P  Q, constant_function(f;A;B), IdLnk, x,y. t(x;y), x. t(x), kindcase(k; a.f(a); l,t.g(l;t) ), Knd, x:A  B(x), P & Q, , r  s, e < e', val-axiom(E;V;M;info;pred?;init;Trans;Choose;Send;val;time), , Msg(M), type List, kind(e), EOrderAxioms(E; pred?; info), EqDecider(T), E, ES, let x,y = A in B(x;y), t.1, , loc(e), discrete state@i, (e < e'), (e <loc e'), e loc e' , True, False, P  Q, P  Q, isrcv(e), Atom$n, P  Q, T, (discrete state when e), x(s), (discrete state after e), e(e1,e2].P(e), e[e1,e2).P(e), s ~ t, SQType(T), {T}, pred(e), A c B, x:A. B(x), first(e), {x:A| B(x)}

Lemmas

es-locl transitivity1, es-causl weakening, member wf, es-first wf, es-next, es-locl transitivity2, es-pred-locl, es-le-pred, es-pred wf, implies functionality wrt iff, all functionality wrt iff, es-le weakening, es-causle-le, Id sq, dstate-after-pred, es-dstate-after wf, squash wf, true wf, event system wf, es-le wf, es-causl wf, es-locl wf, es-dstate-when wf, es-isrcv-loc, es-le-loc, es-loc-pred, es-locl-iff, es-dstate wf, es-loc wf, es-E wf, deq wf, EOrderAxioms wf, Id wf, kind wf, loc wf, Msg wf, nat wf, val-axiom wf, cless wf, qle wf, bool wf, rationals wf, Knd wf, kindcase wf, IdLnk wf, EState wf, constant function wf, not wf, assert wf, first wf, top wf, unit wf